Craig interpolation and uniform interpolation have many applications in knowledge representation, including explainability, forgetting, modularization and reuse, and even learning. At the same time, many relevant knowledge representation formalisms do in general not have Craig or uniform interpolation, and computing interpolants in practice is challenging. We have a closer look at two prominent knowledge representation formalisms, description logics and logic programming, and discuss theoretical results and practical methods for computing interpolants.

We present a method for extracting general modules for ontologies formulated in the description logic ALC. A module for an ontology is an ideally substantially smaller ontology that preserves all entailments for a user-specified set of terms. As such, it has applications such as ontology reuse and ontology analysis. Different from classical modules, general modules may use axioms not explicitly present in the input ontology, which allows for additional conciseness. So far, general modules have only been investigated for lightweight description logics. We present the first work that considers the more expressive description logic ALC. In particular, our contribution is a new method based on uniform interpolation supported by some new theoretical results. Our evaluation indicates that our general modules are often smaller than classical modules and uniform interpolants computed by the state-of-the-art, and compared with uniform interpolants, can be computed in a significantly shorter time. Moreover, our method can be used for, and in fact improves, the computation of uniform interpolants and classical modules.

Abductive reasoning generates explanatory hypotheses for new observations using prior knowledge. This paper investigates the use of forgetting, also known as uniform interpolation, to perform ABox abduction in description logic (ALC) ontologies. Non-abducibles are specified by a forgetting signature which can contain concept, but not role, symbols. The resulting hypotheses are semantically minimal and each consist of a set of disjuncts. These disjuncts are each independent explanations, and are not redundant with respect to the background ontology or the other disjuncts, representing a form of hypothesis space. The observations and hypotheses handled by the method can contain both atomic or complex ALC concepts, excluding role assertions, and are not restricted to Horn clauses. Two approaches to redundancy elimination are explored for practical use: full and approximate. Using a prototype implementation, experiments were performed over a corpus of real world ontologies to investigate the practicality of both approaches across several settings.

Forgetting is an operation on knowledge bases that has been addressed in different areas of Knowledge Representation and with respect to different formalisms, including classical propositional and first-order logic, modal logics, logic programming, and description logics. Definitions of forgetting have been expressed in terms of manipulation of formulas, sets of postulates, isomorphisms between models, bisimulations, second-order quantification, elementary equivalence, and others. In this paper, forgetting is regarded as an abstract belief change operator, independent of the underlying logic. The central thesis is that forgetting amounts to a reduction in the language, specifically the signature, of a logic. The main definition is simple: the result of forgetting a portion of a signature in a theory is given by the set of logical consequences of this theory over the reduced language. This definition offers several advantages. Foremost, it provides a uniform approach to forgetting, with a definition that is applicable to any logic with a well-defined consequence relation. Hence it generalises a disparate set of logic-specific definitions with a general, high-level definition. Results obtained in this approach are thus applicable to all subsumed formal systems, and many results are obtained much more straightforwardly. This view also leads to insights with respect to specific logics: for example, forgetting in first-order logic is somewhat different from the accepted approach. Moreover, the approach clarifies the relation between forgetting and related operations, including belief contraction.

Uniform interpolation and the dual task of forgetting restrict the ontology to a specified subset of concept and role names. This makes them useful tools for ontology analysis, ontology evolution and information hiding. Most previous research focused on uniform interpolation of TBoxes. However, especially for applications in privacy and information hiding, it is essential that uniform interpolation methods can deal with ABoxes as well. We present the first method that can compute uniform interpolants of any ALC ontology with ABoxes. ABoxes bring their own challenges when computing uniform interpolants, possibly requiring disjunctive statements or nominals in the resulting ABox. Our method can compute representations of uniform interpolants in ALCO. An evaluation on realistic ontologies shows that these uniform interpolants can be practically computed, and can often even be presented in pure ALC.

We study (i) uniform interpolation for TBoxes that are formulated in the description logic EL and (ii) approximations of TBoxes formulated in more expressive languages. In both cases, we give model-theoretic characterizations based on simulations and cartesian products, and we develop algorithms that decide whether interpolants and approximations exist. We present a uniform approach to both problems, based on a novel amorphous automaton model called EL automata (EA). Using EAs, we also establish a simpler proof of the known result that conservative extensions of EL-TBoxes can be decided in ExpTime.

We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform interpolants and their existence in terms of bisimulations, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model-theoretic and automata-theoretic methods that, as a by-product, also provides charachterizations of, and decision procedures for, conservative extensions.

We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform inter- polants and their existence in terms of bisimula- tions, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model- theoretic and automata-theoretic methods that, as a by-product, also provides characterizations of and decision procedures for conservative extensions.